Inference at * 1 
Iof proof for Lemma fseg weakening:



1. T : Type
2. l1 : T List
3. l2 : T List
4. l1 = l2
  l2 = ([] @ l1) 

latex

 by ((Reduce 0) 
CollapseTHEN (Auto)) 

latex

C.

Definitions

s = t, type List, Type